Nuprl Lemma : can-apply-mu' 11,40
A:Type, P:(A), d:(x:A. Dec(n:. ((P(x,n))))), x:A.
(can-apply(mu'(P);x))  (n:. ((P(x,n)))) 
latex

ProofTree

Definitionsb, can-apply(f;x), mu'(P), Type, t  T, , , x:AB(x), f(a), x:A. B(x), x:A  B(x), x:A. B(x), Dec(P), p-mu-decider, s ~ t, A, x:A.B(x), Top, False, if b then t else f fi , P  Q, P  Q, P & Q, P  Q, p-mu(P;x), {x:A| B(x)} , True, A c B, left + right, , s = t
Lemmasp-mu-decider, top wf, p-mu wf, true wf, false wf, decidable wf, assert wf, nat wf, bool wf

origin